﻿using System;
using System.Collections.Generic;
using System.Text;
using System.Linq;

using System.Diagnostics.Contracts;

using SimpleIR;
using RgnAnalyzer.Domain;

namespace RgnAnalyzer
{
	/// <summary>
	/// Analyzing each block, loop, body results in completion or suspension with contol returning to an outer processing loop.
	/// These flags indicate these return statuses.
	/// </summary>
	enum LocalAnalysisResult { FrozenForCall, ReturnToLocalProcLoop, LocalComponentComplete };

	/// <summary>
	/// This class represents sets of program models.
	/// </summary>
	public static class LocalAnalyzer
	{
		/////////////////////////////////
		//Methods

#if DEBUG_ENABLED
		private static bool PreBreakTest(int line, MethodContextState mcs)
		{ return (mcs.DebugState >= DebugState.DebugStep) || ((mcs.DebugState == DebugState.DebugBreakAt) && line == GlobalAnalysisState.TAnalysisState.BreakStatementID); }
#else
		private static bool PreBreakTest(int line, MethodContextState mcs)
		{ return false; }
#endif

		private static void ProcessDebugCommandsStmt(IRByteCode bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);
			Contract.Requires(m != null);

			String cmd;
			String sstr = bc.ToString();

			while(true)
			{
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.Display__PrintPendingStateList();
				Console.Write("\nstmt: " + bc.UseModLoc + ", " + sstr + "\n" + "> ");
				cmd = Console.ReadLine();

				if(cmd.Equals("r") || cmd.Equals("run"))
				{
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.DebugState = DebugState.DebugBreakAt;
					break;
				}
				else if(cmd.StartsWith("b ") || cmd.StartsWith("break "))
				{
					int bl = cmd.IndexOf(' ');
					String target = cmd.Substring(bl + 1);
					GlobalAnalysisState.TAnalysisState.BreakStatementID = Int32.Parse(target);
				}
				else if(cmd.Equals("d") || cmd.Equals("display"))
				{
					if(m.IsInfeasable)
						Console.Write("Program flow is infeasable!!!\n");
					else
					{
						Console.Write("******************* Norm Flow State *******************\n");

						if(System.IO.Directory.Exists(System.IO.Path.GetDirectoryName(GlobalAnalysisState.GlobalDataDir)))
						{
							PInfoModel.PIModel pim = m.MakePIModelForThis();
							String dgmlsin = pim.DGMLDumpPModel(bc.UseModLoc - 1);
							System.IO.File.WriteAllText(System.IO.Path.Combine(GlobalAnalysisState.GlobalDataDir, "pmodel.dgml"), dgmlsin);
						}
					}
				}
				else if(cmd.Equals("si") || cmd.Equals("stepinto"))
				{
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.DebugState = DebugState.DebugStepInto;
					break;
				}
				else if(cmd.Equals("s") || cmd.Equals("step"))
				{
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.DebugState = DebugState.DebugStep;
					break;
				}
				else if(cmd.Equals("p") || cmd.Equals("print"))
				{
					String fgdgml = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.CallStateMethodBody.Body.DGMLDisplayString();
					System.IO.File.WriteAllText(System.IO.Path.Combine(GlobalAnalysisState.GlobalDataDir, "flowgraph.dgml"), fgdgml);
				}
				else if(cmd.Equals("cg") || cmd.Equals("callgraph"))
				{
					System.Xml.XmlWriterSettings settings = new System.Xml.XmlWriterSettings { Indent = true, OmitXmlDeclaration = true, CloseOutput = true, Encoding = Encoding.UTF8 };
					
					try
					{
						String ffn = System.IO.Path.GetFullPath(GlobalAnalysisState.GlobalDataDir + "partialcg.dgml");
						if(System.IO.File.Exists(ffn))
							System.IO.File.Delete(ffn);

						using(System.Xml.XmlWriter cgwriter = System.Xml.XmlTextWriter.Create(ffn, settings))
						{
							GlobalAnalysisState.TProg.CallGraph.SerializeToDGML(cgwriter, GlobalAnalysisState.TProg);
						}
					}
					catch(System.IO.IOException)
					{
						Console.WriteLine("Unable to write call graph!!");
					}
				}
				else
				{
					Console.WriteLine("Unknown Command");
					Console.WriteLine("run [r]: Analyze till breakpoint.");
					Console.WriteLine("break [b]: Set a breakpoint at the line/function.");
					Console.WriteLine("display [d]: Display the current analysis state.");
					Console.WriteLine("stepinto [si]: Analyze the stmt, going into call if needed.");
					Console.WriteLine("step [s]: Analyze the stmt, do not go into expressions.");
					Console.WriteLine("print [p]: Display flow graph for the current method.");
					Console.WriteLine("callgraph [cg]: Display the call graph for the program.");
				}
			}
		}

		//////////////////////////////////////////////////////////////
		//Support for flow operations

		/// <summary>
		/// Collapse the state into a single model.
		/// </summary>
		private static AProgramMemory CollapseStates(List<AProgramMemory> mml)
		{
			Contract.Requires(mml != null);
			Contract.Ensures(Contract.Result<AProgramMemory>() != null);

			AProgramMemory res = null;
			for(int i = 0; i < mml.Count; ++i)
			{
				if(mml[i].IsInfeasable)
					continue;

				mml[i].NormalizeLocalFlow(true);
				if(res == null)
					res = mml[i];
				else
					res = AProgramMemory.PMemoryMergeLocalFlow(res, mml[i], false);
			}

			mml.Clear();
			
			return (res == null ? AProgramMemory.MakeInfeasibleFlowProgMemory() : res);
		}

		/// <summary>
		/// Merge this state into the accumulated return in the call stack.
		/// </summary>
		private static void MergeReturnState(MethodContextState mcs, AProgramMemory retv)
		{
			Contract.Requires(mcs != null);

			mcs.UpdateCurrentApprox(retv);
		}

		//////////////////////////////////////////////////////////////
		//Analyze Statements 

		/// <summary>
		/// Start the analysis of a given body with the given model.
		/// </summary>
		internal static LocalAnalysisResult AnalyzeBodyStart(IRBodyDef bdf, AProgramMemory m)
		{
			Contract.Requires(bdf != null);
			Contract.Requires(m != null && (!m.IsInfeasable));

			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.ResetAnalysisInformation();
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushT1T2RegionForAnalysis(bdf.Body.T1T2Body);

			LocalAnalysisResult done = AnalyzeTopoSectionFlow(m);

			if(done == LocalAnalysisResult.LocalComponentComplete)
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();

			if(done == LocalAnalysisResult.ReturnToLocalProcLoop)
				done = AnalyzeBodyResume();

			if(done == LocalAnalysisResult.LocalComponentComplete)
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.ResetAnalysisInformation();
			
			return done;
		}

		internal static LocalAnalysisResult AnalyzeBodyResume()
		{
			MethodEvalState evalst = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState;

			while(!evalst.LocalAnalysisComplete)
			{
				T1T2RegionEvalState pst = evalst.CurrentT1T2EvalRegion;
				LocalAnalysisResult done;

				if(pst is T1T2BasicBlockEvalState)
					done = AnalyzeBlockBody(evalst.FrozenCallResumeModel);
				else if(pst is T1T2BlockEvalState)
					done = AnalyzeTopoSectionFlow(null);
				else
					done = AnalyzeLoop();

				if(done == LocalAnalysisResult.FrozenForCall)
				{
					MethodEvalState.Display__PrintEvalLoopFrozenForCall(GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.DebugState);
					return done;
				}
				else if(done == LocalAnalysisResult.LocalComponentComplete)
				{
					MethodEvalState.Display__PrintEvalLoopPopCompleteComponent(GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.DebugState);
					evalst.PopCompletedT1T2Region();
				}
				else //something new was pushed and we want to process that first
				{
					MethodEvalState.Display__PrintEvalLoopReturnForEvalOfPush(GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.DebugState);
				}
			}

			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.ResetAnalysisInformation();
			return LocalAnalysisResult.LocalComponentComplete;
		}

		/// <summary>
		/// Analyze a single basic block based on the states on the pred edges and set the states on the succ edges.
		/// Also takes an optional extra model for any additional state we want at the start of the block analysis.
		/// The <c>enclosingregion</c> is the region that <c>bb</c> lives in.
		/// </summary>
		private static AProgramMemory AnalyzeBlockDoEntryStateMng(IRBasicBlock bb, IRT1T2Region enclosingregion, int line, AProgramMemory extramodel)
		{
			Contract.Requires(bb != null);
			Contract.Requires(enclosingregion != null);
			
			List<AProgramMemory> mmodelv = new List<AProgramMemory>();
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.FetchAllIncommingFlowEdgeModels(bb.BlockID, mmodelv);

			if(extramodel != null)
				mmodelv.Add(extramodel);
			
			//tidy up state
			for(int i = 0; i < mmodelv.Count; ++i)
				mmodelv[i].ClearVarsNotInScopeAddNew(bb.VarsInScopeAtEntry, bb.VarsLiveAtEntry, bb.BlockVarsToTypeMap, line);
			
			return CollapseStates(mmodelv);
		}

		/// <summary>
		/// Start or Resume the analysis of a basic block (which is the current pending flow component on the local eval stack).
		/// Return true if we complete the analysis of the block, false if we froze the state to analyze a call.
		/// </summary>
		private static LocalAnalysisResult AnalyzeBlockBody(AProgramMemory m)
		{
			Contract.Requires(m != null);

			T1T2BasicBlockEvalState bbes = (T1T2BasicBlockEvalState)GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.CurrentT1T2EvalRegion;

			//The intial input to the block is infeasible, so we are done.
			if(m.IsInfeasable)
				return LocalAnalysisResult.LocalComponentComplete;

			for(int i = bbes.CurrentSubRegionIndex; i < bbes.BasicBlock.Operations.Count; ++i)
			{
				bbes.CurrentSubRegionIndex = i;
				LocalAnalysisResult done = AnalyzeStmt(bbes.BasicBlock.BlockID, bbes.BasicBlock.Operations[i], m);

				if(done != LocalAnalysisResult.LocalComponentComplete)
					return done;
			}

			return LocalAnalysisResult.LocalComponentComplete;
		}

		/// <summary>
		/// Start or Resume the analysis of a T1T2BLock (which is the current pending flow component on the local eval stack).
		/// Return true if we complete the analysis of the block, false if we froze the state to analyze a call or encountered a nested control 
		/// flow structure.
		/// </summary>
		private static LocalAnalysisResult AnalyzeTopoSectionFlow(AProgramMemory extram)
		{
			T1T2BlockEvalState blckst = (T1T2BlockEvalState)GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.CurrentT1T2EvalRegion;
			
			//topo ordered list of loops and basic blocks, simply process in order.
			List<IRT1T2Region> trb = blckst.T1T2Block.T1T2Blocks;
			for(int i = blckst.CurrentSubRegionIndex; i < trb.Count; ++i)
			{
				blckst.CurrentSubRegionIndex = i + 1;
				if(trb[i] is IRBasicBlock)
				{
					IRBasicBlock bb = (IRBasicBlock)trb[i];
					AProgramMemory m;
					if(bb.BlockID != 0)
						m = AnalyzeBlockDoEntryStateMng(bb, blckst.T1T2Block, bb.BlockEntryUseModLoc, null);
					else
						m = AnalyzeBlockDoEntryStateMng(bb, blckst.T1T2Block, bb.BlockEntryUseModLoc, extram);

					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushBasicBlockForAnalysis(bb);
					
					LocalAnalysisResult done = AnalyzeBlockBody(m);

					if(done != LocalAnalysisResult.LocalComponentComplete)
						return done;

					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();
				}
				else
				{
					//push the loop and return to the outer driver loop
					IRT1T2Loop ll = (IRT1T2Loop)trb[i];
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushT1T2RegionForAnalysis(ll);
					return LocalAnalysisResult.ReturnToLocalProcLoop;
				}
			}

			return LocalAnalysisResult.LocalComponentComplete;
		}

		/// <summary>
		/// Start or Resume the analysis of a T1T2Loop (which is the current pending flow component on the local eval stack).
		/// Return true if we complete the analysis of the loop, false if we froze the state to analyze a call or encountered a nested control 
		/// flow structure.
		/// </summary>
		private static LocalAnalysisResult AnalyzeLoop()
		{
			T1T2LoopEvalState ll = (T1T2LoopEvalState)GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.CurrentT1T2EvalRegion;
			
			if(ll.CurrentlyAnalysisResumeState == T1T2LoopEvalState.LoopResumeState.InitializeLoopInit)
			{
				ll.OrigLoopEntryPModelApprox = AnalyzeBlockDoEntryStateMng(ll.T1T2Loop.Head, ll.T1T2Loop, ll.T1T2Loop.Head.BlockEntryUseModLoc, null);

				//The intial input to the loop is infeasible, so we are done.
				if(ll.OrigLoopEntryPModelApprox.IsInfeasable)
					return LocalAnalysisResult.LocalComponentComplete;

				ll.CurrentPModelApprox = ll.OrigLoopEntryPModelApprox.CopyMemoryState();
				ll.LastPModelApprox = ll.OrigLoopEntryPModelApprox.CopyMemoryState();
				ll.CurrentlyAnalysisResumeState = T1T2LoopEvalState.LoopResumeState.ResumeInHead;
			}
			
			while((ll.CurrentlyAnalysisResumeState != T1T2LoopEvalState.LoopResumeState.ResumeAtTest) || (!AProgramMemory.EquivOnLoopFix(ll.CurrentPModelApprox, ll.LastPModelApprox)))
			{
				//if we resumed at the test and it failed then we update the last approx model and continue
				if(ll.CurrentlyAnalysisResumeState == T1T2LoopEvalState.LoopResumeState.ResumeAtTest)
				{
					ll.CurrentlyAnalysisResumeState = T1T2LoopEvalState.LoopResumeState.ResumeInHead;
					ll.LastPModelApprox = ll.CurrentPModelApprox.CopyMemoryState();
				}

				if(ll.CurrentlyAnalysisResumeState == T1T2LoopEvalState.LoopResumeState.ResumeInHead)
				{
					ll.CurrentlyAnalysisResumeState = T1T2LoopEvalState.LoopResumeState.ResumeInBody;
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushBasicBlockForAnalysis(ll.T1T2Loop.Head);
					
					UpdateUseModAllocAndTraverseOnLoopBackFlow(ll.CurrentPModelApprox, ll);
					ll.CurrentPModelApprox.NormalizeLocalFlow(true);

					LocalAnalysisResult done = AnalyzeBlockBody(ll.CurrentPModelApprox);
					if(done != LocalAnalysisResult.LocalComponentComplete)
						return done;

					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();
				}

				if(ll.CurrentlyAnalysisResumeState == T1T2LoopEvalState.LoopResumeState.ResumeInBody)
				{
					ll.CurrentlyAnalysisResumeState = T1T2LoopEvalState.LoopResumeState.ResumeInPostLoopJoin;
					if(!ll.T1T2Loop.IsSelfLoopOnHead)
					{
						//push the body and return to the outer processing loop
						GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushT1T2RegionForAnalysis(ll.T1T2Loop.LoopBody);
						return LocalAnalysisResult.ReturnToLocalProcLoop;
					}
				}

				ll.CurrentlyAnalysisResumeState = T1T2LoopEvalState.LoopResumeState.ResumeAtTest;
				AProgramMemory mmnh = AnalyzeBlockDoEntryStateMng(ll.T1T2Loop.Head, ll.T1T2Loop, ll.T1T2Loop.Head.BlockEntryUseModLoc, null);

				if(!mmnh.IsInfeasable)
					ll.CurrentPModelApprox = AProgramMemory.PMemoryMergeLocalFlow(ll.LastPModelApprox, mmnh, false);
				else
					ll.CurrentPModelApprox = ll.LastPModelApprox.CopyMemoryState();

				ll.LoopIterCtr++;
			}

			/////
			//Keep track of the body enter states
			if(ll.CurrentPModelApprox != null)
			{
				AProgramMemory entrypm = ll.CurrentPModelApprox.CopyMemoryState();
				UpdateUseModAllocAndTraverseOnLoopBackFlow(entrypm, ll);
				entrypm.NormalizeLocalFlow(true);

				if(!GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.LoopToEntryInvStateMap.ContainsKey(ll.T1T2Loop.Head.BlockID))
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.LoopToEntryInvStateMap.Add(ll.T1T2Loop.Head.BlockID, entrypm);
				else
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.LoopToEntryInvStateMap[ll.T1T2Loop.Head.BlockID] = entrypm;
			}

			////
			//clean up and return 
			if(ll.LoopIterCtr > GlobalAnalysisState.MaxLoopFixIters)
				GlobalAnalysisState.MaxLoopFixIters = ll.LoopIterCtr;

			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.UpdateFlowLocationsAndClearLoopTraversalInfoOnLoopExit(ll);

			return LocalAnalysisResult.LocalComponentComplete;
		}

		/// <summary>
		/// On the back edge for a loop update all the information that we need to do for modeling 
		/// loop previous iteration use/mod, allocation, and traversal bits.
		/// </summary>
		private static void UpdateUseModAllocAndTraverseOnLoopBackFlow(AProgramMemory pm, T1T2LoopEvalState loopstate)
		{
			IRT1T2Loop ll = loopstate.T1T2Loop;
			int minstmt = ll.MinStmt();
			int maxstmt = ll.MaxStmt();

			//first update the use/mod and allocation info
			pm.AdvanceUseModAndAllocInfoToLoopPrevious(minstmt, maxstmt, ll.LoopLastIterUseModLoc);
		}

		/// <summary>
		/// On the advance operations for a loop traverse increment the position info for each entry.
		/// </summary>
		private static void AdvanceTraverseOnIndexOperation(AProgramMemory pm, IRT1T2Loop ll)
		{
			int minstmt = ll.MinStmt();
			int maxstmt = ll.MaxStmt();

			IRVarName indexname = (ll.IndexerStoreLoc != null ? ll.IndexerStoreLoc.LocalVar : null);
			int okindexmod = (ll.IndexerStoreLoc != null ? ll.IndexerStoreLoc.UseModLoc : -1);
			pm.AdvanceLoopPositionInfo(ll.ContainerCopyVar, ll.OptContainerCopyField, indexname, minstmt, maxstmt, okindexmod);
		}

		/// <summary>
		/// Analyze a single stmt.
		/// Resume the analysis of a single bytecode statement, which is passed in, on the given model.
		/// Return true if we complete the analysis of the bytecode (and <c>m</c> is modified), false if we froze 
		/// the state to analyze a call (in which case <c>m</c> remains unchanged).
		/// </summary>
		[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Maintainability", "CA1505:AvoidUnmaintainableCode")]
		[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Maintainability", "CA1502:AvoidExcessiveComplexity")]
		private static LocalAnalysisResult AnalyzeStmt(long currentblock, IRByteCode bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);

			if(PreBreakTest(bc.UseModLoc, GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState))
			{
				Console.WriteLine("\nBefore Stmt Analysis");
				ProcessDebugCommandsStmt(bc, m);
			}

			if(m.IsInfeasable)
				return LocalAnalysisResult.LocalComponentComplete;

			LocalAnalysisResult localres;
			switch(bc.OperationCode)
			{
				case OpCode.Op.BranchU:
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.SetFlowEdgeModel(currentblock, ((IRBranchOp)bc).BRUTarget, m);
					break;
				case OpCode.Op.BranchC:
					LocalAnalyzer.AnalyzeBranchCond(currentblock, (IRBranchOp)bc, m);
					break;
				case OpCode.Op.Switch:
					LocalAnalyzer.AnalyzeSwitch(currentblock, (IRBranchOp)bc, m);
					break;
				case OpCode.Op.Throw:
					m.SetInfeasable();
					break;
				case OpCode.Op.Return:
					LocalAnalyzer.AnalyzeReturn((IRBranchOp)bc, m);
					break;
				case OpCode.Op.Call:
					if(((IRCallOp)bc).InvokeSig.IsVirtualInvoke)
						localres = LocalAnalyzer.AnalyzeVirtualCall((IRCallOp)bc, m);
 					else
						localres = LocalAnalyzer.AnalyzeStaticCall((IRCallOp)bc, m);

					if(localres == LocalAnalysisResult.FrozenForCall)
						return localres;
					break;
				case OpCode.Op.CallVirt:
					IRCallOp invbc = ((IRCallOp)bc);
					if(invbc.ReciverExpType is IRPtrType && ((IRPtrType)invbc.ReciverExpType).PtrTargetType is IRLambdaType && invbc.InvokeSig.InvokeName.Equals("Invoke"))
						localres = LocalAnalyzer.AnalyzeLambdaInvoke((IRCallOp)bc, m);
					else
						localres = LocalAnalyzer.AnalyzeVirtualCall((IRCallOp)bc, m);
					
					if(localres == LocalAnalysisResult.FrozenForCall)
						return localres;
					break;
				case OpCode.Op.AllocCons:
					localres = LocalAnalyzer.AnalyzeAllocObj((IRAllocationOp)bc, m);
					if(localres == LocalAnalysisResult.FrozenForCall)
						return localres;
					break;
				case OpCode.Op.PrimEQ:
					m.SimulatePrimEQ();
					break;
				case OpCode.Op.Less:
				case OpCode.Op.LessU:
					m.SimulateLess();
					break;
				case OpCode.Op.LessEQ:
				case OpCode.Op.LessEQU:
					m.SimulateLessEQ();
					break;
				case OpCode.Op.Greater:
				case OpCode.Op.GreaterU:
					m.SimulateGreater();
					break;
				case OpCode.Op.GreaterEQ:
				case OpCode.Op.GreaterEQU:
					m.SimulateGreaterEQ();
					break;
				case OpCode.Op.Add:
				case OpCode.Op.AddU:
				case OpCode.Op.Div:
				case OpCode.Op.DivU:
				case OpCode.Op.Mult:
				case OpCode.Op.MultU:
					m.SimulateUninterpBin();
					break;
				case OpCode.Op.Neg:
					m.SimulateUninterpUnary();
					break;
				case OpCode.Op.Rem:
				case OpCode.Op.RemU:
				case OpCode.Op.Sub:
				case OpCode.Op.SubU:
					m.SimulateUninterpBin();
					break;
				case OpCode.Op.And:
					m.SimulateAnd();
					break;
				case OpCode.Op.Or:
					m.SimulateOr();
					break;
				case OpCode.Op.Not:
					m.SimulateUninterpUnary();
					break;
				case OpCode.Op.Shl:
				case OpCode.Op.Shr:
				case OpCode.Op.ShrU:
				case OpCode.Op.Xor:
					m.SimulateUninterpBin();
					break;
				case OpCode.Op.Conv:
					m.SimulateConvOp((IRNumericType)((IREvalStackTypeOp)bc).TypeArg);
					break;
				case OpCode.Op.LoadFromLocal:
					m.SimulateLoadFromLocal(((IRLoadToEvalStackBasic)bc).LocalVar, ((IRLoadToEvalStackBasic)bc).IsLocalDeadAfterLoad, bc.UseModLoc);
					break;
				case OpCode.Op.StoreToLocal:
					m.SimulateStoreToLocal(((IRStoreFromEvalStackBasic)bc).LocalVar, bc.UseModLoc);
					if(((IRStoreFromEvalStackBasic)bc).IsTraverseLoopIndexAdvance)
						AdvanceTraverseOnIndexOperation(m, GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.GetCurrentOutermostLoop());
					break;
				case OpCode.Op.LoadFromGlobal:
					m.SimulateLoadFromGlobal(((IRLoadToEvalStackBasic)bc).StaticField, bc.UseModLoc);
					break;
				case OpCode.Op.StoreToGlobal:
					m.SimulateStoreToGlobal(((IRStoreFromEvalStackBasic)bc).StaticField, bc.UseModLoc);
					break;
				case OpCode.Op.ArrayLoad:
					m.SimulateArrayLoad(bc.UseModLoc, ((IRLoadToEvalStackIndirect)bc).ArrayLoadType.ContainerContentsType);
					SetCurrentContainerAccessAsNeeded(bc, null, m);
					break;
				case OpCode.Op.ArrayStore:
					m.SimulateArrayStore(bc.UseModLoc, ((IRStoreFromEvalStackIndirect)bc).ArrayStoreType.ContainerContentsType);
					break;
				case OpCode.Op.ArrayLength:
					m.SimulateArrayLength(bc.UseModLoc);
					break;
				case OpCode.Op.IndirectRead:
					m.SimulateDeRefIndirectRead(bc.UseModLoc);
					break;
				case OpCode.Op.IndirectWrite:
					m.SimulateDeRefIndirectWrite(bc.UseModLoc);
					break;
				case OpCode.Op.LoadMemberField:
					m.SimulateIndexAddrByField(((IRLoadToEvalStackIndirect)bc).LoadField, 0);
					if(!m.IsInfeasable)
						m.SimulateDeRefIndirectRead(bc.UseModLoc);
					break;
				case OpCode.Op.StoreMemberField:
					m.SimulateIndexAddrByField(((IRStoreFromEvalStackIndirect)bc).WriteField, 1);
					if(!m.IsInfeasable)
						m.SimulateDeRefIndirectWrite(bc.UseModLoc);
					break;
				case OpCode.Op.IndirectInitialize:
					m.SimulateDeRefIndirectInitialize(((IRStoreFromEvalStackIndirect)bc).ThroughRefType.ReferenceTargetType, bc.UseModLoc);
					break;
				case OpCode.Op.LoadStructField:
					m.SimulateReadFromStructOnStack(((IRLoadToEvalStackIndirect)bc).LoadField, bc.UseModLoc);
					break;
				case OpCode.Op.LoadLocalAddr:
					m.SimulateLoadLocalAddr(((IRPointerIndexOp)bc).LocalName);
					break;
				case OpCode.Op.LoadGlobalAddr:
					m.SimulateLoadGlobalAddr(((IRLoadToEvalStackBasic)bc).StaticField);
					break;
				case OpCode.Op.IndexRefAddrByField:
					m.SimulateIndexAddrByField(((IRPointerIndexOp)bc).IndexField, ((IRPointerIndexOp)bc).StackIndexOfDeRefable);
					break;
				case OpCode.Op.IndexRefAddrByArrayIndex:
					m.SimulateIndexAddrInsideArray(((IRPointerIndexOp)bc).ArrayType.ContentsField);
					break;
				case OpCode.Op.LoadFuncPtr:
					m.SimulateLoadFuncPtr(((IRLoadToEvalStackBasic)bc).InvokeIdentity);
					break;
				case OpCode.Op.LoadVFuncPtr:
					DebugReport.ReportError("Load VFunc pointer Not Supported Yet.");
					break;
				case OpCode.Op.DerefableEQ:
					m.SimulateDrefableEQ();
					break;
				case OpCode.Op.NonNull:
					m.SimulatePointerNonNull();
					break;
				case OpCode.Op.Box:
					m.SimulateBox((IRValueType)((IREvalStackTypeOp)bc).TypeArg, bc.UseModLoc);
					break;
				case OpCode.Op.UnBox:
					m.SimulateUnBox((IRValueType)((IREvalStackTypeOp)bc).TypeArg, -1);
					break;
				case OpCode.Op.Cast:
					m.SimulateCast((IRPtrType)((IREvalStackTypeOp)bc).TypeArg, bc.UseModLoc);
					break;
				case OpCode.Op.IsInst:
					m.SimulateIsInst((IRPtrType)((IREvalStackTypeOp)bc).TypeArg, bc.UseModLoc);
					break;
				case OpCode.Op.Constrain:
					m.SimulateConstrain(((IREvalStackTypeOp)bc).TypeArg, ((IREvalStackTypeOp)bc).ConstrainPos, bc.UseModLoc);
					break;
				case OpCode.Op.Pop:
					m.SimulatePop();
					break;
				case OpCode.Op.Dup:
					m.SimulateDup();
					break;
				case OpCode.Op.PushNull:
					m.SimulatePushNull();
					break;
				case OpCode.Op.PushInt:
				case OpCode.Op.PushFloat:
					SimulateLoadConstToStack((IRLoadToEvalStackBasic)bc, m);
					break;
				case OpCode.Op.PushString:
					m.SimulatePushString(bc.UseModLoc);
					break;
				default:
					DebugReport.ReportError("Bad Op in analyze switch.");
					break;
			}

			m.CheckConsistent();

			return LocalAnalysisResult.LocalComponentComplete;
		}

		/// <summary>
		/// On return from calls and array loads, check if the result is a current container get and 
		/// mark the result as appropriate.
		/// </summary>
		private static void SetCurrentContainerAccessAsNeeded(IRByteCode bc, IRBodyDef invbody, AProgramMemory m)
		{
			if(m.IsInfeasable)
				return;

			bool isarraytraverseload = ((bc is IRLoadToEvalStackIndirect) && ((IRLoadToEvalStackIndirect)bc).IsLoopTraverseGet);
			bool istraversecallload = ((bc is IRCallOp) && ((IRCallOp)bc).IsLoopTraverseGet);
			if(!(isarraytraverseload | istraversecallload))
				return;

			IRT1T2Loop ll = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.GetCurrentOutermostLoop();
			IRVarName root = ll.ContainerCopyVar;
			IRMemberField optf = ll.OptContainerCopyField;
			IRVarName optindex = (ll.IndexerStoreLoc != null ? ll.IndexerStoreLoc.LocalVar : null);
			int loopmin = ll.MinStmt();
			int loopmax = ll.MaxStmt();
			int indexpos = (ll.IndexerStoreLoc != null ? ll.IndexerStoreLoc.UseModLoc : -1);

			bool indexget = (invbody == null) || (invbody.Qualifier & MethodQualifiers.GetIndexer) != MethodQualifiers.Clear;
			bool enumcollectionget = (invbody != null) && (invbody.Qualifier & MethodQualifiers.EnumeratorGetterSimpleContainer) != MethodQualifiers.Clear;
			bool enumdictget = (invbody != null) && (invbody.Qualifier & MethodQualifiers.EnumeratorGetterDictionary) != MethodQualifiers.Clear;
			bool enumdictkeyget = (invbody != null) && (invbody.Qualifier & MethodQualifiers.EnumeratorGetterDictionaryKeys) != MethodQualifiers.Clear;
			bool enumdictvalget = (invbody != null) && (invbody.Qualifier & MethodQualifiers.EnumeratorGetterSimpleDictionaryValues) != MethodQualifiers.Clear;

			m.SetStackTopAsLoopTraverseCurrent(root, optf, optindex, loopmin, loopmax, indexpos, indexget, enumcollectionget, enumdictget, enumdictkeyget, enumdictvalget);
		}

		private static void AnalyzeBranchCond(long currentblock, IRBranchOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);
			Contract.Requires(m != null && (!m.IsInfeasable));

			Tuple<AProgramMemory, AProgramMemory> truefalseresult = m.SplitOnExpTruthBoolVal();
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.SetFlowEdgeModel(currentblock, ((IRBranchOp)bc).BRCondTrueTarget, truefalseresult.Item1);
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.SetFlowEdgeModel(currentblock, ((IRBranchOp)bc).BRCondFalseTarget, truefalseresult.Item2);
		}

		private static void AnalyzeSwitch(long currentblock, IRBranchOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);
			Contract.Requires(m != null && (!m.IsInfeasable));

			AProgramMemory[] switchsplit = m.SplitForSwitch(bc.SwitchTargets.Length);
			for(int i = 0; i < bc.SwitchTargets.Length; ++i)
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.SetFlowEdgeModel(currentblock, bc.SwitchTargets[i], switchsplit[i]);
		}

		private static void SimulateLoadConstToStack(IRLoadToEvalStackBasic bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);
			Contract.Requires(m != null && (!m.IsInfeasable));

			IRLiteralExp litval = bc.Literal;
			Contract.Assert(litval.LiteralType is IRPrimitiveType);

			IRPrimitiveType pv = (IRPrimitiveType)litval.LiteralType;
			if(pv is IRSignedIntegerType || pv is IRUnSignedIntegerType)
				m.SimulatePushInt(litval.IntVal);
			else
				m.SimulatePushFloat(litval.FloatVal);
		}

		private static LocalAnalysisResult AnalyzeVirtualCall(IRCallOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null, "for pure virtual");
			Contract.Requires(m != null && (!m.IsInfeasable));

			LocalAnalysisResult finalres = LocalAnalysisResult.LocalComponentComplete;

			if(!m.IsVCallNonNull(bc.InvokeSig.InvokeSig.Count + 1))
			{
				m.SetInfeasable();
				return finalres;
			}

			List<AProgramMemory> spm = new List<AProgramMemory>();
			m.DoCallArgTargetUniqueify(bc.InvokeSig.InvokeSig.Count + 1, spm);
			List<AProgramMemory> respm = new List<AProgramMemory>();

			GlobalAnalysisState.Display__CallToSig(bc.InvokeSig);

			for(int i = 0; i < spm.Count; ++i)
			{
				AProgramMemory mproc = spm[i];
				List<IRType> argtl = bc.InvokeSig.InvokeSig;
				int stackstart = mproc.GetFirstLocalStackPosForCall(argtl.Count + 1);
				IRType stckrcvr = mproc.GetTargetEvalStackRcvrType(bc.InvokeSig.InvokeSig.Count + 1);
				mproc.AssertVCallTargetNonNull(bc.InvokeSig.InvokeSig.Count + 1);

				Tuple<IRType, IRInvokeSig> nettypeandsig = new Tuple<IRType, IRInvokeSig>(bc.BaseImplementationType, bc.InvokeSig);
				IRBodyDef bd;
				IRType contexttoken;
				if(stckrcvr is IRReferenceType)
				{
					bd = GlobalAnalysisState.TProg.GetBodyForClassAndSig(((IRReferenceType)stckrcvr).ReferenceTargetType, nettypeandsig);
					contexttoken = ((IRReferenceType)stckrcvr).ReferenceTargetType;
				}
				else
				{
					IRClassType actualimpltype = mproc.GetTargetCallClassForName(stackstart, bc.UseModLoc);
					contexttoken = actualimpltype;

					//if we have a specific target but that doesn't match the type we found in the node, well then just skip it
					if((bc.HasSpecificTarget) && (!bc.SpecificTargetClass.TypeDescription.AllSubTypes.Contains(actualimpltype)))
						continue;

					IRType actualImplClass;
					if(actualimpltype is IRBoxedType)
					{
						IRValueType btv = ((IRBoxedType)actualimpltype).BoxedTypeValue;
						IRType baselookuptype = (bc.HasSpecificTarget ? bc.SpecificTargetClass : btv);
						actualImplClass = IRProgram.GetImplClassWithThisAsBaseType(baselookuptype, nettypeandsig);

						mproc.SimulateUnBox(btv, stackstart);
					}
					else
					{
						mproc.SetArgType(GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor((IRClassType)actualimpltype), stackstart);
						IRType baselookuptype = (bc.HasSpecificTarget ? bc.SpecificTargetClass : actualimpltype);
						actualImplClass = IRProgram.GetImplClassWithThisAsBaseType(baselookuptype, nettypeandsig);
					}

					bd = GlobalAnalysisState.TProg.GetBodyForClassAndSig(actualImplClass, nettypeandsig);
				}

				for(int j = 0; j < argtl.Count; ++j)
				{
					IRType tt = argtl[j];
					mproc.SetArgType(tt, stackstart + 1 + j);
				}

				LocalAnalysisResult lar = LocalAnalyzer.DoAnalyzeOfCall(mproc, bc, bd, contexttoken, false, bc.UseModLoc);

				if(lar == LocalAnalysisResult.FrozenForCall)
					finalres = LocalAnalysisResult.FrozenForCall;

				if(!mproc.IsInfeasable)
					respm.Add(mproc);
			}

			if(finalres != LocalAnalysisResult.FrozenForCall)
			{
				if(respm.Count == 1)
					m.AssignIntoThis(respm[0]);
				else
					m.AssignIntoThis(LocalAnalyzer.CollapseStates(respm));
			}
			else
			{
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.FrozenCallResumeModel = m.CopyMemoryState();
				m.SetInfeasable();
			}

			return finalres;
		}

		private static LocalAnalysisResult AnalyzeLambdaInvoke(IRCallOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null && (bc.InvokeSig.IsVirtualInvoke));
			Contract.Requires(m != null && (!m.IsInfeasable));

			LocalAnalysisResult finalres = LocalAnalysisResult.LocalComponentComplete;
			GlobalAnalysisState.Display__CallToSig(bc.InvokeSig);

			List<AProgramMemory> spm = new List<AProgramMemory>();
			List<AProgramMemory> respm = new List<AProgramMemory>();
			m.DoCallArgTargetUniqueify(bc.InvokeSig.InvokeSig.Count + 1, spm);

			for(int i = 0; i < spm.Count; ++i)
			{
				List<IRType> argtl = bc.InvokeSig.InvokeSig;
				int stackstart = spm[i].GetFirstLocalStackPosForCall(argtl.Count + 1);
				HashSet<IRInvokeIdentity> iivs = spm[i].GetLambdaInvokeTargets(stackstart, bc.UseModLoc);

				foreach(IRInvokeIdentity iid in iivs)
				{
					AProgramMemory mproc = (iivs.Count == 1 ? spm[i] : spm[i].CopyMemoryState());
					Tuple<IRType, IRInvokeSig> nettypeandsig = new Tuple<IRType, IRInvokeSig>(iid.DefInClass, iid.Sig);
					IRBodyDef bd = GlobalAnalysisState.TProg.GetBodyForClassAndSig(iid.DefInClass, nettypeandsig);

					for(int j = 0; j < argtl.Count; ++j)
					{
						IRType tt = argtl[j];
						mproc.SetArgType(tt, stackstart + 1 + j);
					}

					mproc.PopOrConvertLambdaAsNeeded(stackstart, iid);

					LocalAnalysisResult lar = LocalAnalyzer.DoAnalyzeOfCall(mproc, bc, bd, bd.InvokeID.DefInClass, false, bc.UseModLoc);

					if(lar == LocalAnalysisResult.FrozenForCall)
						finalres = LocalAnalysisResult.FrozenForCall;

					if(!mproc.IsInfeasable)
						respm.Add(mproc);
				}
			}

			if(finalres != LocalAnalysisResult.FrozenForCall)
			{
				if(respm.Count == 1)
					m.AssignIntoThis(respm[0]);
				else
					m.AssignIntoThis(LocalAnalyzer.CollapseStates(respm));
			}
			else
			{
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.FrozenCallResumeModel = m.CopyMemoryState();
				m.SetInfeasable();
			}

			return finalres; 
		}

		private static LocalAnalysisResult AnalyzeStaticCall(IRCallOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null && (bc.InvokeSig.IsStaticInvoke));
			Contract.Requires(m != null && (!m.IsInfeasable));

			GlobalAnalysisState.Display__CallToSig(bc.InvokeSig);

			AProgramMemory mproc = m.CopyMemoryState();
			Tuple<IRType, IRInvokeSig> nettypeandsig = new Tuple<IRType, IRInvokeSig>(bc.SpecificTargetClass, bc.InvokeSig);
			IRBodyDef bd = GlobalAnalysisState.TProg.GetBodyForClassAndSig(bc.SpecificTargetClass, nettypeandsig);
			List<IRType> argtl = bc.InvokeSig.InvokeSig;
			int stackstart = mproc.GetFirstLocalStackPosForCall(argtl.Count);

			for(int j = 0; j < argtl.Count; ++j)
			{
				IRType tt = argtl[j];
				mproc.SetArgType(tt, stackstart + j);
			}

			LocalAnalysisResult lar = LocalAnalyzer.DoAnalyzeOfCall(mproc, bc, bd, bd.InvokeID.DefInClass, false, bc.UseModLoc);

			if(lar != LocalAnalysisResult.FrozenForCall)
				m.AssignIntoThis(mproc);
			else
			{
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.FrozenCallResumeModel = m.CopyMemoryState();
				m.SetInfeasable();
			}

			return lar;
		}

		private static LocalAnalysisResult AnalyzeAllocObj(IRAllocationOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);
			Contract.Requires(m != null && (!m.IsInfeasable));

			if(bc.IsArrayAlloc)
			{
				m.EvalStackPop();
				m.SimulateAllocBlank(bc.AllocType, bc.UseModLoc);
				return LocalAnalysisResult.LocalComponentComplete;
			}
			else if(bc.AllocType is IRLambdaType)
			{
				m.SimulateAllocDelegate((IRLambdaType)bc.AllocType, bc.UseModLoc);
				return LocalAnalysisResult.LocalComponentComplete;
			}
			else
			{
				Tuple<IRType, IRInvokeSig> nettypeandsig = new Tuple<IRType, IRInvokeSig>(bc.AllocType, bc.ConsIdentity.Sig);
				IRBodyDef bd = GlobalAnalysisState.TProg.GetBodyForClassAndSig(bc.AllocType, nettypeandsig);
				List<IRType> argtl = bc.ConsIdentity.Sig.InvokeSig;

				AProgramMemory nnpm = m.CopyMemoryState();
				nnpm.SimulateAllocBlank(bc.AllocType, bc.UseModLoc);
				if(bc.AllocType is IRStructType)
				{
					nnpm.SimulateBox((IRValueType)bc.AllocType, bc.UseModLoc);
					nnpm.SimulateUnBox((IRValueType)bc.AllocType, -1);
				}

				int stackstart = nnpm.GetFirstLocalStackPosForCall(argtl.Count + 1);
				nnpm.RotateBlankAllocToRecvrPosition(stackstart);

				GlobalAnalysisState.Display__CallToSig(bc.ConsIdentity.Sig);

				for(int j = 0; j < argtl.Count; ++j)
				{
					IRType tt = argtl[j];
					nnpm.SetArgType(tt, stackstart + 1 + j);
				}

				LocalAnalysisResult lar = LocalAnalyzer.DoAnalyzeOfCall(nnpm, bc, bd, bc.AllocType, true, bc.UseModLoc);

				if(lar != LocalAnalysisResult.FrozenForCall)
					m.AssignIntoThis(nnpm);
				else
				{
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.FrozenCallResumeModel = m.CopyMemoryState();
					m.SetInfeasable();
				}

				return lar;
			}
		}

		private static void AnalyzeReturn(IRBranchOp bc, AProgramMemory m)
		{
			Contract.Requires(bc != null);
			Contract.Requires(m != null && (!m.IsInfeasable));

			MethodContextState mcs = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState;
			LocalAnalyzer.MergeReturnState(mcs, m);
		}

		//////////////////////////////////////////////////////////////
		//Support for Inter-procedural Analysis

		/// <summary>
		/// Move from the caller scope into the callee scope, setting the parameter names and as needed unboxing the reciver argument
		/// <c>rcvrtype</c> is ignored if the method is actually static for static methods.
		/// </summary>
		private static void MoveIntoCalleeScope(AProgramMemory m, IRBodyDef calledBody)
		{
			Contract.Requires(m != null && (!m.IsInfeasable));
			Contract.Requires(calledBody != null);

			for(int i = calledBody.Parameters.Count - 1; i >= 0; --i)
				m.PopStackArgIntoLocalName(calledBody.Parameters[i], calledBody.InvokeID.Sig.InvokeSig[i], calledBody.Body.T1T2Body.MinStmt());

			if(calledBody.InvokeID.Sig.IsVirtualInvoke)
			{
				if(calledBody.InvokeID.DefInClass is IRValueType)
					m.PopStackArgIntoLocalName(GlobalAnalysisState.TProg.NameTable.LookupLocalVarName("this"), GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(calledBody.InvokeID.DefInClass), calledBody.Body.T1T2Body.MinStmt());
				else
					m.PopStackArgIntoLocalName(GlobalAnalysisState.TProg.NameTable.LookupLocalVarName("this"), GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor((IRClassType)calledBody.InvokeID.DefInClass), calledBody.Body.T1T2Body.MinStmt());
			}

			m.ClearArgStack();
		}

		/// <summary>
		/// Analyze a builtin method.
		/// </summary>
		private static void AnalyzeBuiltin(AProgramMemory m, IRBodyDef calledMethod, bool isconsinvoke, int line)
		{
			Contract.Requires(m != null && (!m.IsInfeasable));
			Contract.Requires(calledMethod != null);

			GlobalAnalysisState.Display__BuiltinExec(calledMethod.InvokeID);

			IRInvokeIdentity caller = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.MethodOfCallState;
			if(!GlobalAnalysisState.TProg.CallGraph.ResolvedCallEdgeAlreadyAdded(caller, calledMethod.InvokeID))
				GlobalAnalysisState.TProg.CallGraph.AddAnalysisResolvedCallEdge(caller, calledMethod.InvokeID);

			//exec builtin op
			m.SimulateBuiltinCall(calledMethod, line, isconsinvoke);
		}

		/// <summary>
		/// Analyze a call that is on a dag edge in the call graph.
		/// </summary>
		private static LocalAnalysisResult AnalyzeSimpleCall(AProgramMemory m, IRBodyDef calledMethod, IRType contexttoken)
		{
			Contract.Requires(m != null && (!m.IsInfeasable));
			Contract.Requires(calledMethod != null);

			IRInvokeIdentity caller = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.MethodOfCallState;
			if(!GlobalAnalysisState.TProg.CallGraph.ResolvedCallEdgeAlreadyAdded(caller, calledMethod.InvokeID))
				GlobalAnalysisState.TProg.CallGraph.AddAnalysisResolvedCallEdge(caller, calledMethod.InvokeID);

			CallStateSubMap csm = new CallStateSubMap();
			MethodContextState memop = GlobalAnalysisState.TAnalysisState.HasMemoForCallAddMemoContextAsNeeded(calledMethod, m, false, contexttoken, csm);
			Contract.Assert((csm.OutCase == MatchCase.FreshMatch) | (csm.OutCase == MatchCase.EqualityMatch), "Should always be one of the two.");

			//manage the mappings from the callertospecific callee scope as needed in final pass
			if(GlobalAnalysisState.CompleteAnalysisResults != null)
				FinalPassManageCallStateMappings(memop, csm);

			if(csm.OutCase == MatchCase.EqualityMatch)
			{
				GlobalAnalysisState.Display__Memoized(calledMethod.InvokeID);
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.ContextIDsUsedCurrentPass.Add(memop);

				AProgramMemory resm = memop.GetCopyOfOutputStateApplyMaps(csm);
				m.AssignIntoThis(resm);
				return LocalAnalysisResult.LocalComponentComplete;
			}
			else
			{
				//push this onto the pending list
				GlobalAnalysisState.Display__FullyResolvedPendingForCall(calledMethod.InvokeID);
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.ContextIDPendingNotYetDep = memop;
				GlobalAnalysisState.TAnalysisState.EnqueueCalleeMethod(memop, GlobalAnalysisState.TProg.CallGraph);

				return LocalAnalysisResult.FrozenForCall;
			}
		}

		/// <summary>
		/// Analyze a call which is part of a scc in the call graph.
		/// </summary>
		private static LocalAnalysisResult AnalyzeSCCCall(AProgramMemory m, IRBodyDef calledMethod, IRType contexttoken)
		{
			Contract.Requires(m != null && (!m.IsInfeasable));
			Contract.Requires(calledMethod != null);

			IRInvokeIdentity caller = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.MethodOfCallState;
			if(!GlobalAnalysisState.TProg.CallGraph.ResolvedCallEdgeAlreadyAdded(caller, calledMethod.InvokeID))
				GlobalAnalysisState.TProg.CallGraph.AddAnalysisResolvedCallEdge(caller, calledMethod.InvokeID);

			CallStateSubMap csm = new CallStateSubMap();
			MethodContextState memop = GlobalAnalysisState.TAnalysisState.HasMemoForCallAddMemoContextAsNeeded(calledMethod, m, true, contexttoken, csm);

			//manage the mappings from the callertospecific callee scope as needed in final pass
			if(GlobalAnalysisState.CompleteAnalysisResults != null)
				FinalPassManageCallStateMappings(memop, csm);

			if(csm.OutCase == MatchCase.FreshMatch)
			{
				GlobalAnalysisState.Display__GeneralPendingForCall(calledMethod.InvokeID);
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.ContextIDPendingNotYetDep = memop;
				GlobalAnalysisState.TAnalysisState.EnqueueCalleeMethod(memop, GlobalAnalysisState.TProg.CallGraph);

				return LocalAnalysisResult.FrozenForCall;
			}
			else
			{
				GlobalAnalysisState.Display__Memoized(calledMethod.InvokeID);
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.ContextIDsUsedCurrentPass.Add(memop);

				if(csm.OutCase == MatchCase.SubsumeAlter)
				{
					GlobalAnalysisState.TAnalysisState.EnqueueCalleeMethod(memop, GlobalAnalysisState.TProg.CallGraph);
					
					return LocalAnalysisResult.FrozenForCall;
				}
				else
				{
					//just get the current approximate result and go with it
					AProgramMemory resm = memop.GetCopyOfOutputStateApplyMaps(csm);
					m.AssignIntoThis(resm);
					
					return LocalAnalysisResult.LocalComponentComplete;
				}
			}
		}

		private static void FinalPassManageCallStateMappings(MethodContextState memop, CallStateSubMap csm)
		{
			Contract.Requires(csm.OutCase == MatchCase.EqualityMatch || csm.OutCase == MatchCase.SubsumeMatch);

			//reverse the map
			Dictionary<int, int> ttm = new Dictionary<int, int>();
			foreach(KeyValuePair<int, HashSet<int>> ii in csm.ResMap)
			{
				foreach(int jj in ii.Value)
					ttm.Add(jj, ii.Key);
			}

			//reverse the map
			Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>> erfmap = new Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>>();
			foreach(KeyValuePair<AExternalRef, HashSet<AExternalRef>> err in csm.ExtRefMap)
			{
				PInfoModel.PIExternalRef newt = new PInfoModel.PIExternalRef(err.Key.IDTAG, err.Key.StaticRef);
				foreach(AExternalRef er in err.Value)
				{
					if(!erfmap.ContainsKey(newt))
						erfmap.Add(newt, new HashSet<PInfoModel.PIExternalRef>());
					erfmap[newt].Add(new PInfoModel.PIExternalRef(er.IDTAG, er.StaticRef));
				}
			}

			PInfoModel.CompleteAnalysisInfoMethodContext calleectx = GlobalAnalysisState.CompleteAnalysisResults.LookupInfoForMethodAndContext(memop.MethodOfCallState, memop.ContextID);
			calleectx.UpdateCallersForCallee(GlobalAnalysisState.CompleteAnalysisResults.CurrentContext, ttm);
		}

		internal static LocalAnalysisResult DoAnalyzeOfCall(AProgramMemory pm, IRByteCode bc, IRBodyDef b, IRType contexttoken, bool isconsinvoke, int line)
		{
			Contract.Requires(pm != null && (!pm.IsInfeasable));
			Contract.Requires(b != null);

			if(bc is IRCallOp)
				((IRCallOp)bc).AnalysisResolvedCallTargets.Add(b.InvokeID);

			if(b.IsBuiltin)
			{
				LocalAnalyzer.AnalyzeBuiltin(pm, b, isconsinvoke, line);

				if(bc is IRCallOp)
				{
					SetCurrentContainerAccessAsNeeded(bc, b, pm);
					Contract.Assert(!((IRCallOp)bc).IsTraverseLoopIndexAdvance, "We Don't support builtin Enumerator Advance!!");
				}

				return LocalAnalysisResult.LocalComponentComplete;
			}
			else
			{
				IRInvokeIdentity currentinvoke = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.MethodOfCallState;
				bool inreccycle = GlobalAnalysisState.TProg.CallGraph.IsCallInSCC_StaticCallGraph(b.InvokeID);

				//if we are in final info pass set up call line info
				if(GlobalAnalysisState.CompleteAnalysisResults != null)
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.InitializeCallInfoProcessAtLine(bc.UseModLoc, GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.InvokeID, GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.ContextID, b.InvokeID);

				//compute the set of all static vars that we need (if this is not fully resolved then leave as null to indicate all are ok).
				HashSet<IRStaticField> ursf = new HashSet<IRStaticField>(b.UsedModStaticFields);

				//project
				IRInvokeSig sig = b.InvokeID.Sig;
				int argc = ((sig is IRVirtualInvoke) ? sig.InvokeSig.Count + 1 : sig.InvokeSig.Count);
				List<AExternalRef> newrefs = new List<AExternalRef>();
				Dictionary<int, Tuple<List<UseModInfo>, int[], EscapeSiteInfo[]>> callstatemappings = new Dictionary<int, Tuple<List<UseModInfo>, int[], EscapeSiteInfo[]>>();
				
				AProgramMemory reachm = pm.ExtractReachableCallGraph(argc, ursf, newrefs, inreccycle, line);
				MoveIntoCalleeScope(reachm, b);

				AProgramMemory reachunmod = reachm.CopyMemoryState();

				if(!inreccycle)
					reachm.NormalizeAtSimpleCallEntry();
				else
				{
					reachm.CheckByRefFreeForRecCalls();
					reachm.NormalizeAtRecursiveCallEntry();
				}

				List<Tuple<AExternalRef, AExternalRef>> cptidymap = reachm.CPTidyAtCall();

				bool cleartraverse = (b.Qualifier & MethodQualifiers.DoNotClearTraverse) == MethodQualifiers.Clear;
				reachm.ProcessRegionInfoForMoveIntoCalleeScope(callstatemappings, cleartraverse);

				//////
				LocalAnalysisResult rr;
				if(inreccycle)
					rr = LocalAnalyzer.AnalyzeSCCCall(reachm, b, contexttoken);
				else
					rr = LocalAnalyzer.AnalyzeSimpleCall(reachm, b, contexttoken);

				//reprocess info and extend as needed
				if(rr != LocalAnalysisResult.FrozenForCall)
				{
					if(!inreccycle && !reachm.IsInfeasable)
					{
						reachunmod.ReachEliminateLocsWhichAreSubjectToStrongUpdates();
						reachunmod.NormalizeLocalFlow(false);
					}
					else
					{
						reachunmod.ClearLocalsOnReturn();
						reachunmod.NormalizeLocalFlow(false);
					}

					if(isconsinvoke)
					{
						if(!reachm.IsInfeasable)
							reachm.PopInitializedRefBackToStackReturn(b.InvokeID.DefInClass, line);

						if(b.InvokeID.DefInClass is IRClassType)
							reachunmod.ReturnBaseCaseWithWeakUpdates(GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor((IRClassType)b.InvokeID.DefInClass));
						else
							reachunmod.ReturnBaseCaseWithWeakUpdates(b.InvokeID.DefInClass);
					}
					else
						reachunmod.ReturnBaseCaseWithWeakUpdates(b.ReturnType);

					if(reachm.IsInfeasable)
						pm.MergeReachableCallGraphIntoThis(reachunmod, newrefs);
					else
					{
						reachm.ClearLocalsOnReturn();
						reachm.NormalizeLocalFlow(false);
						reachm.RestoreCallerScopeIdsExtendEscapeInfo(callstatemappings, line);
						reachm.CPTidyAtCallRevert(cptidymap);

						AProgramMemory finalm = AProgramMemory.PMemoryMergeLocalFlow(reachm, reachunmod, true);
						pm.MergeReachableCallGraphIntoThis(finalm, newrefs);
					}

					if(bc is IRCallOp)
					{
						SetCurrentContainerAccessAsNeeded(bc, b, pm);
						if(((IRCallOp)bc).IsTraverseLoopIndexAdvance)
							AdvanceTraverseOnIndexOperation(pm, GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.GetCurrentOutermostLoop());
					}
				}

				//if we are in final info pass build the final sets of caller to/from callee mappings
				if(GlobalAnalysisState.CompleteAnalysisResults != null)
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.FinalizeCallerCalleeMappings();

				return rr;
			}
		}

		/////////////////////////////////
		//Methods for completing program information

		/// <summary>
		/// Start the analysis of a given body with the given model -- compute the complete program info for the context.
		/// </summary>
		internal static void InfoComplete_AnalyzeBody(IRBodyDef bdf, AProgramMemory pm, bool computeprogpointinfo)
		{
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.ResetAnalysisInformation();
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushT1T2RegionForAnalysis(bdf.Body.T1T2Body);

			InfoComplete_AnalyzeTopoSectionFlow(pm, computeprogpointinfo);
			
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.ResetAnalysisInformation();
		}

		/// <summary>
		/// Start or Resume the analysis of a basic block (which is the current pending flow component on the local eval stack).
		/// Return true if we complete the analysis of the block, false if we froze the state to analyze a call.
		/// </summary>
		private static void InfoComplete_AnalyzeBlockBody(AProgramMemory m, bool computeprogpointinfo)
		{
			Contract.Requires(m != null);

			T1T2BasicBlockEvalState bbes = (T1T2BasicBlockEvalState)GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.CurrentT1T2EvalRegion;

			//The intial input to the block is infeasible, so we are done.
			if(m.IsInfeasable)
				return;

			if(computeprogpointinfo)
			{
				PInfoModel.PIModel entrymodel = m.MakePIModelForThis();
				if(!GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.BlockIDToStateMap.ContainsKey(bbes.BasicBlock.BlockID))
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.BlockIDToStateMap.Add(bbes.BasicBlock.BlockID, entrymodel);
				else
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.BlockIDToStateMap[bbes.BasicBlock.BlockID] = entrymodel;
			}

			PInfoModel.PIModel prem = computeprogpointinfo ? m.MakePIModelForThis() : null;
			PInfoModel.PIModel postm = null;

			for(int i = bbes.CurrentSubRegionIndex; i < bbes.BasicBlock.Operations.Count; ++i)
			{
				bbes.CurrentSubRegionIndex = i;
				LocalAnalysisResult done = AnalyzeStmt(bbes.BasicBlock.BlockID, bbes.BasicBlock.Operations[i], m);
				Contract.Assert(done == LocalAnalysisResult.LocalComponentComplete);

				if(computeprogpointinfo)
				{
					if(m == null || m.IsInfeasable)
						postm = null;
					else
						postm = m.MakePIModelForThis();

					PInfoModel.ProgramPointInfo ppi = new PInfoModel.ProgramPointInfo(prem, postm);
					prem = postm;
					postm = null;

					if(!GlobalAnalysisState.CompleteAnalysisResults.CurrentProgramPointInfo.ContainsKey(bbes.BasicBlock.Operations[i].UseModLoc))
						GlobalAnalysisState.CompleteAnalysisResults.CurrentProgramPointInfo.Add(bbes.BasicBlock.Operations[i].UseModLoc, ppi);
					else
						GlobalAnalysisState.CompleteAnalysisResults.CurrentProgramPointInfo[bbes.BasicBlock.Operations[i].UseModLoc] = ppi;
				}
			}
		}

		/// <summary>
		/// Start or Resume the analysis of a T1T2BLock (which is the current pending flow component on the local eval stack).
		/// Return true if we complete the analysis of the block, false if we froze the state to analyze a call or encountered a nested control 
		/// flow structure.
		/// </summary>
		private static void InfoComplete_AnalyzeTopoSectionFlow(AProgramMemory extram, bool computeprogpointinfo)
		{
			T1T2BlockEvalState blckst = (T1T2BlockEvalState)GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.CurrentT1T2EvalRegion;

			//topo ordered list of loops and basic blocks, simply process in order.
			List<IRT1T2Region> trb = blckst.T1T2Block.T1T2Blocks;
			for(int i = blckst.CurrentSubRegionIndex; i < trb.Count; ++i)
			{
				blckst.CurrentSubRegionIndex = i + 1;
				if(trb[i] is IRBasicBlock)
				{
					IRBasicBlock bb = (IRBasicBlock)trb[i];
					AProgramMemory m;
					if(bb.BlockID != 0)
						m = AnalyzeBlockDoEntryStateMng(bb, blckst.T1T2Block, bb.BlockEntryUseModLoc, null);
					else
						m = AnalyzeBlockDoEntryStateMng(bb, blckst.T1T2Block, bb.BlockEntryUseModLoc, extram);

					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushBasicBlockForAnalysis(bb);

					InfoComplete_AnalyzeBlockBody(m, computeprogpointinfo);

					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();
				}
				else
				{
					//push the loop and return to the outer driver loop
					IRT1T2Loop ll = (IRT1T2Loop)trb[i];
					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushT1T2RegionForAnalysis(ll);

					InfoComplete_AnalyzeLoop(computeprogpointinfo);

					GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();
				}
			}
		}

		/// <summary>
		/// Start or Resume the analysis of a T1T2Loop (which is the current pending flow component on the local eval stack).
		/// Return true if we complete the analysis of the loop, false if we froze the state to analyze a call or encountered a nested control 
		/// flow structure.
		/// </summary>
		private static void InfoComplete_AnalyzeLoop(bool computeprogpointinfo)
		{
			T1T2LoopEvalState ll = (T1T2LoopEvalState)GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.CurrentT1T2EvalRegion;
			long loopheadid = ll.T1T2Loop.Head.BlockID;

			//The intial input to the loop is infeasible, so we are done.
			if(!GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.LoopToEntryInvStateMap.ContainsKey(loopheadid))
				return;

			ll.CurrentPModelApprox = GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.LoopToEntryInvStateMap[loopheadid].CopyMemoryState();
			
			////
			//no need to loop just once through and we are done
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushBasicBlockForAnalysis(ll.T1T2Loop.Head);
			InfoComplete_AnalyzeBlockBody(ll.CurrentPModelApprox, computeprogpointinfo);
			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();

			if(!ll.T1T2Loop.IsSelfLoopOnHead)
			{
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PushT1T2RegionForAnalysis(ll.T1T2Loop.LoopBody);
				InfoComplete_AnalyzeTopoSectionFlow(null, computeprogpointinfo);
				GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.PopCompletedT1T2Region();
			}

			GlobalAnalysisState.TAnalysisState.CurrentMethodEvalState.BodyEvalState.UpdateFlowLocationsAndClearLoopTraversalInfoOnLoopExit(ll);
		}
	}
}
